| Definitions |  x:A. B(x), P   Q, EOrderAxioms(E; pred?; info), P & Q, A & B, t  T, Top, S  T,  x:A. B(x), P  Q, Prop, SQType(T), {T}, sends(l;e), snds(l;t), concat(ll), map(f;as), m(l;t), upto(n), Y, if b t else f fi, true , reduce(f;k;as),  , false,  b, null(as), True,  A, A B, False, i j, ||as||, rcvs(l;t), filter(P;l), i=j, E, 1of(t), 2of(t),  x. t(x), isrcv(l;a), p  q, b, time(e), loc(e),  T, P  Q, P Q, first(e), pred(e), SWellFounded(R(x;y)), rcv?(e), w-info(w;e), sender(e), link(e), ecase1(e;info;i.f(i);l,e'.g(l;e')), kindcase(k; a.f(a); l,t.g(l;t) ), sender(e), lnk(k), rcv(l,tg), islocal(k), act(k), outl(x), tag(k), isl(x), outr(x), locl(a), isrcv(k), {i..j }, i j < k, Msg, Dec(P),  , Unit, FairFifo, x(s), Knd,  |
| Lemmas | fair-fifo wf, world wf, decidable assert, null wf3, w-sends wf, top wf, w-Msg wf, IdLnk wf, w-E wf, link wf, w-info wf, sender wf, assert wf, rcv? wf, Id wf, cless wf, w-pred wf, loc wf, ldst wf, IdLnk sq, w-match-sender, w-match wf, w-time wf, assert of null, assert-w-match, w-loc-sender, lsrc wf, Id sq, w-loc-lemma, length wf1, w-action wf, w-rcvs wf, w-snds wf, w-snd-rcv, non neg length, nat wf, eq int wf, bool wf, iff transitivity, eqtt to assert, assert of eq int, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, map append sq, int seg wf, upto wf, concat append, map wf, w-ml wf, le wf, append-nil, decidable equal Id, w-loc wf, length-append, pos length, nat properties, ge wf, filter append sq, w-isrcvl wf, w-a wf, filter wf, subtype rel list, w-isnull wf, pi1 wf, pi2 wf, false wf, isrcv wf, w-kind wf, eq lnk wf, lnk wf, decidable le, upto decomp, squash wf, true wf, w-loc-rcv, or functionality wrt iff, w-cless-loc, decidable lt, w-pred-bound, unit wf, isl wf, w-pred-decreases, outl wf, w-pred!-decreases, pred! wf, w-loc-w-pred, w-cless-decreases, w-ekind wf, Knd wf, w-match-exists, Knd sq, mu wf, w-match-unique, mu-property, iseg length, filter iseg, iseg map, upto iseg, w-onlnk-m, length append, w-onlnk wf, w-m wf, Msg wf, w-M wf, mlnk wf, concat-cons, append nil sq, concat iseg |